(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


From Coquelicot Require Import Complex.
Require Import Reals.
Open Scope R_scope.
Require Import Matrix.Mat.Mat_make.
Require Export Matrix.Mat.Matrix_Module.

Section Lemma_needed.

Lemma Cplus_assoc2 : forall x y z w:Complex.C ,
  ((x+y)+(z+w))%C = ((x+z)+(y+w))%C.
Proof. intros. ring. Qed.

Lemma Cplus_assoc': forall x y z : Complex.C,
  (x + y + z)%C = (x + (y + z))%C.
Proof. intros. ring. Qed.

Lemma Cminus_0_l: forall x :Complex.C, (0-x)%C = (-x)%C.
Proof. intros. ring. Qed.

Lemma Cminus_0_r: forall x :Complex.C, (x-0)%C = (x)%C.
Proof. intros. ring. Qed.

Lemma Cminus_assoc : forall x y z:Complex.C, 
  (x - y - z)%C = ( x - (y + z))%C.
Proof. intros. ring. Qed.

Lemma Cminus_assoc2: forall x y z w ,
  ((x+y)-(z+w))%C = ((x-z)+(y-w))%C.
Proof. intros. ring. Qed.

Lemma Cminus_opp : forall x y ,(x - y)%C = (-(y - x))%C.
Proof. intros. ring. Qed.

Lemma Cminus_self : forall x , (x - x)%C = 0.
Proof. intros. ring. Qed. 

Lemma Cmult_distr_l : forall x y z, ((x+y)*z)%C = (x*z + y*z)%C.
Proof. intros. ring. Qed.

Lemma Cmult_distr_r : forall x y z, (x*(y+z))%C = (x*y + x *z)%C. 
Proof. intros. ring. Qed.

Lemma Cmult_add_distr_l : forall x y z, ((x+y)*z)%C = (x*z + y*z)%C.
Proof. intros. ring. Qed.

Lemma Cmult_add_distr_r : forall x y z, (x*(y+z))%C = (x*y + x *z)%C. 
Proof. intros. ring. Qed.

Lemma Cmult_sub_distr_l : forall x y z, ((x-y)*z)%C = (x*z - y*z)%C.
Proof. intros. ring. Qed.

Lemma Cmult_sub_distr_r : forall x y z, (x*(y-z))%C = (x*y - x *z)%C. 
Proof. intros. ring. Qed.

Lemma Cmult_assoc': forall x y z : Complex.C,
       (x * y * z)%C = (x * (y * z))%C.
Proof. intros. ring. Qed.

End Lemma_needed.

Module CM.
Definition A := Complex.C.

Definition One := RtoC 1.
Definition Zero := RtoC 0.

Definition opp := Copp.
Definition add := Cplus.
Definition sub := Cminus.
Definition mul := Cmult.

Definition add_comm := Cplus_comm.
Definition add_assoc := Cplus_assoc'.
Definition add_zero_l := Cplus_0_l.
Definition add_zero_r := Cplus_0_r.

Definition add_assoc2 := Cplus_assoc2.
Definition sub_assoc := Cminus_assoc.
Definition sub_assoc2:= Cminus_assoc2.
Definition sub_opp := Cminus_opp.
Definition sub_zero_l:= Cminus_0_l.
Definition sub_zero_r:= Cminus_0_r.
Definition sub_self:= Cminus_self.

Definition mul_add_distr_l:= Cmult_add_distr_l.
Definition mul_add_distr_r := Cmult_add_distr_r.
Definition mul_sub_distr_l := Cmult_sub_distr_l.
Definition mul_sub_distr_r := Cmult_sub_distr_r.
Definition mul_assoc := Cmult_assoc'.
Definition mul_zero_l := Cmult_0_l.
Definition mul_zero_r := Cmult_0_r.
Definition mul_one_l:= Cmult_1_l.
Definition mul_one_r:= Cmult_1_r.
Definition mul_comm := Cmult_comm.

End CM.

Module CMatrix := Matrix(CM).

Definition CMtrans := @CMatrix.Mtrans.
Arguments CMtrans {m} {n}.

Definition CMadd := @CMatrix.Madd.
Arguments CMadd {m} {n}.

Definition CMsub := @CMatrix.Msub.
Arguments CMsub {m} {n}.

Definition CMopp := @CMatrix.Mopp.
Arguments CMopp {m} {n}.

Definition CMmul := @CMatrix.Mmul.
Arguments CMmul {m} {n} {p}.

Definition CMmulc_l := @CMatrix.Mmulc_l.
Arguments CMmulc_l {m} {n}.

Definition CMmulc_r := @CMatrix.Mmulc_r.
Arguments CMmulc_r {m} {n}.

Definition CMO := @CMatrix.MO.

Definition CMI := @CMatrix.MI.

Notation "m1 CM+ m2" := (CMadd m1 m2) (at level 65).

Notation "m1 CM- m2" := (CMsub m1 m2) (at level 65).

Notation " CM- m" := (CMopp m) (at level 65).

Notation "m1 CM* m2" := (CMmul m1 m2) (at level 60).

Notation "c CC* m" := (CMmulc_l c m) (at level 60).

Notation "m *CC c" := (CMmulc_r m c) (at level 60).

(*Definition CMeq_visit := @CMatrix.Meq_visit.
Arguments CMeq_visit {m} {n}. *)

Definition CMadd_comm := @CMatrix.Madd_comm.
Arguments CMadd_comm {m} {n}.

Definition CMadd_assoc := @CMatrix.Madd_assoc.
Arguments CMadd_assoc {m} {n}.

Definition CMadd_zero_l := @CMatrix.Madd_zero_l.
Arguments CMadd_zero_l {m} {n}.

Definition CMadd_zero_r := @CMatrix.Madd_zero_r.
Arguments CMadd_zero_r {m} {n}.

Definition CMsub_comm := @CMatrix.Msub_comm.
Arguments CMsub_comm {m} {n}.

Definition CMsub_assoc := @CMatrix.Msub_assoc.
Arguments CMsub_assoc {m} {n}.

Definition CMsub_O_l := @CMatrix.Msub_O_l.
Arguments CMsub_O_l {m} {n}.

Definition CMsub_O_r := @CMatrix.Msub_O_r.
Arguments CMsub_O_r {m} {n}.

Definition CMsub_self := @CMatrix.Msub_self.
Arguments CMsub_self {m} {n}.

Definition CMmul_distr := @CMatrix.Mmul_add_distr_l.
Arguments CMmul_distr {m} {n}.

Definition CMmul_assoc:= @CMatrix.Mmul_assoc.
Arguments CMmul_assoc {m} {n} {p} {k}.

Definition CMmul_zero_l:=@CMatrix.Mmul_zero_l.
Arguments CMmul_zero_l {m} {n}.

Definition CMmul_zero_r:=@CMatrix.Mmul_zero_r.
Arguments CMmul_zero_r {m}{n}.

Definition CMmul_mul_unit_l := @CMatrix.Mmul_unit_l.
Arguments CMmul_mul_unit_l {m} {n}.

Definition CMmul_mul_unit_r := @CMatrix.Mmul_unit_r.
Arguments CMmul_mul_unit_r {m} {n}.

Definition CMmulc_comm := @CMatrix.Mmulc_comm.
Arguments CMmulc_comm {m} {n}.

Definition CMmulc_distr_l :=@CMatrix.Mmulc_distr_l.
Arguments CMmulc_distr_l {m} {n}.

Definition CMmulc_0_l:=@CMatrix.Mmulc_0_l.
Arguments CMmulc_0_l {m} {n}.

Definition CMtteq := @CMatrix.Mtteq.
Arguments CMtteq {m} {n}.

Definition CMcteq := @CMatrix.Mcteq.
Arguments CMcteq {m} {n}.

Definition CMteq_add := @CMatrix.Mteq_add.
Arguments CMteq_add {m} {n}.

Definition CMteq_sub := @CMatrix.Mteq_sub.
Arguments CMteq_sub {m} {n}.

Definition CMteq_mul := @CMatrix.Mteq_mul.
Arguments CMteq_mul {m} {n}.

Definition CMtrans_MI:= @CMatrix.Mtrans_MI.
Arguments CMtrans_MI {n}.

Require Export Setoid.
Require Export Relation_Definitions.
Set Implicit Arguments.

Add Parametric Relation {m n:nat} : (Mat (Complex.C) m n) (@M_eq (Complex.C) m n) 
  reflexivity proved by (@Meq_ref (Complex.C) m n)
  symmetry proved by (@Meq_sym (Complex.C) m n)
  transitivity proved by (@Meq_trans (Complex.C) m n)
  as CMeq_rel.


Lemma Cmat_add_compat : 
  forall m n, 
     forall x x' : (Mat (Complex.C) m n ), @M_eq (Complex.C) m n x x' ->
     forall y y' : (Mat (Complex.C) m n ), @M_eq (Complex.C) m n y y'->
        @M_eq (Complex.C) m n (CMadd x y) (CMadd x' y').
Proof.
  intros.
  unfold CMadd,CMatrix.Madd. rewrite H,H0.
  reflexivity.
Qed.

Add Parametric Morphism {m n :nat}:(@CMadd m n)
  with signature (@M_eq (Complex.C) m n) ==> 
  (@M_eq (Complex.C) m n) ==> (@M_eq (Complex.C) m n) 
  as Cmat_add_mor.
Proof.
exact (@Cmat_add_compat m n).
Qed.

Lemma Cmat_sub_compat : 
  forall m n, 
     forall x x' : (Mat (Complex.C) m n ), @M_eq (Complex.C) m n x x' ->
     forall y y' : (Mat (Complex.C) m n ), @M_eq (Complex.C) m n y y'->
        @M_eq (Complex.C) m n (CMsub x y) (CMsub x' y').
Proof.
  intros.
  unfold CMsub,CMatrix.Msub. rewrite H,H0.
  reflexivity.
Qed.

Add Parametric Morphism {m n :nat}:(@CMsub m n)
  with signature (@M_eq (Complex.C) m n) 
    ==> (@M_eq (Complex.C) m n) ==> (@M_eq (Complex.C) m n) 
  as Cmat_sub_mor.
Proof.
exact (@Cmat_sub_compat m n).
Qed.

Lemma Cmat_opp_compat : 
  forall m n, 
     forall x x' : (Mat (Complex.C) m n ), @M_eq (Complex.C) m n x x' ->
        @M_eq (Complex.C) m n (CMopp x ) (CMopp x' ).
Proof.
  intros.
  unfold CMopp,CMatrix.Mopp. rewrite H.
  reflexivity.
Qed.

Add Parametric Morphism {m n :nat}:(@CMopp m n)
  with signature (@M_eq (Complex.C) m n) ==> (@M_eq (Complex.C) m n)
  as Cmat_opp_mor.
Proof.
exact (@Cmat_opp_compat m n).
Qed.

Lemma Cmat_trans_compat : 
  forall m n, 
     forall x x' : (Mat (Complex.C) m n ), @M_eq (Complex.C) m n x x' ->
        @M_eq (Complex.C) n m (CMtrans x ) (CMtrans x' ).
Proof.
  intros.
  unfold CMtrans,CMatrix.Mtrans. rewrite H.
  reflexivity.
Qed.

Add Parametric Morphism {m n :nat}:(@CMtrans m n)
  with signature (@M_eq (Complex.C) m n) ==> (@M_eq (Complex.C) n m)
  as Cmat_trans_mor.
Proof.
exact (@Cmat_trans_compat m n).
Qed.

Lemma Cmat_mul_compat : 
  forall m n p, 
     forall x x' : (Mat (Complex.C) m n ), @M_eq (Complex.C) m n x x' ->
     forall y y' : (Mat (Complex.C) n p ), @M_eq (Complex.C) n p y y'->
        @M_eq (Complex.C) m p (CMmul x y) (CMmul x' y').
Proof.
  intros.
  unfold CMmul,CMatrix.Mmul. rewrite H,H0.
  reflexivity.
Qed.

Add Parametric Morphism {m n p :nat}:(@CMmul m n p)
  with signature (@M_eq (Complex.C) m n) 
    ==> (@M_eq (Complex.C) n p) ==> (@M_eq (Complex.C) m p) 
  as Cmat_mul_mor.
Proof.
exact (@Cmat_mul_compat m n p).
Qed.

(* Section test.

Variable m n:nat.
Variable tm1 tm2 tm3 tm4:Mat Complex.C m n.
Axiom a1: tm1 === tm3.

Axiom a2: tm2 === tm4.
Lemma a3: tm1 CM+ tm2 === tm3 CM+ tm4.
Proof. rewrite a1. rewrite a2. apply M_eq_ref. Qed.

End test. *)





